1  (PRED (SUCC N-0)=(N-0)∧∀N1.(PRED (SUCC N-N1)=(N-N1)⊃PRED (SUCC N-SUCC N1)=(N-SUCC N1)))⊃∀N1.PRED (SUCC N-N1)=%
(N-N1)    ∧I (INDUCTION) 

2  (N-0)=N    ∀E MINUS2 N 

3  (SUCC N-0)=SUCC N    ∀E MINUS2 SUCC N 

4  PRED SUCC N=N    ∀E PEANO2 N 

5  (PRED (SUCC N-0)=N∧∀N1.(PRED (SUCC N-N1)=(N-N1)⊃PRED (SUCC N-SUCC N1)=(N-SUCC N1)))⊃∀N1.PRED (SUCC N-N1)=(N-N%
1)    SUBSTR 2 IN 1 

6  (PRED SUCC N=N∧∀N1.(PRED (SUCC N-N1)=(N-N1)⊃PRED (SUCC N-SUCC N1)=(N-SUCC N1)))⊃∀N1.PRED (SUCC N-N1)=(N-N1)  %
  SUBSTR 3 IN 5 

7  ∀N1.(PRED (SUCC N-N1)=(N-N1)⊃PRED (SUCC N-SUCC N1)=(N-SUCC N1))⊃∀N1.PRED (SUCC N-N1)=(N-N1)    TAUT 

8  PRED (SUCC N-N1)=(N-N1)⊃PRED (SUCC N-SUCC N1)=(N-SUCC N1)  (8)  ASSUME 

9  (N-SUCC N1)=PRED (N-N1)    ∀E MINUS3 N , N1 

10  PRED (SUCC N-N1)=(N-N1)  (10)  ASSUME 

11  (N-SUCC N1)=PRED PRED (SUCC N-N1)  (10)  SUBST 10 IN 9 

12  (SUCC N-SUCC N1)=PRED (SUCC N-N1)    ∀E MINUS3 SUCC N , N1 

13  (N-SUCC N1)=PRED (SUCC N-SUCC N1)  (10)  SUBST 12 IN 11 

14  PRED (SUCC N-N1)=(N-N1)⊃(N-SUCC N1)=PRED (SUCC N-SUCC N1)    ⊃I 10 13 

15  PRED (SUCC N-N1)=(N-N1)⊃PRED (SUCC N-SUCC N1)=(N-SUCC N1)    TAUTEQ 

16  ∀N1.(PRED (SUCC N-N1)=(N-N1)⊃PRED (SUCC N-SUCC N1)=(N-SUCC N1))    ∀I 15 N1 ← N1 

17  ∀N1.PRED (SUCC N-N1)=(N-N1)    ⊃E 16 7 

18  PRED (SUCC N-N1)=(N-N1)    ∀E 17 N1 

19  (SUCC N-SUCC N1)=(N-N1)    SUBST 12 IN 18 

20  ((0-0)=0∧∀N.((N-N)=0⊃(SUCC N-SUCC N)=0))⊃∀N.(N-N)=0    ∧I (INDUCTION) 

21  (0-0)=0    ∀E MINUS2 0 

22  (N-N)=0  (22)  ASSUME 

23  ∀N1.(SUCC N-SUCC N1)=(N-N1)    ∀I 19 N1 ← N1 

24  (SUCC N-SUCC N)=(N-N)    ∀E 23 N 

25  (SUCC N-SUCC N)=0  (22)  SUBST 24 IN 22 

26  (N-N)=0⊃(SUCC N-SUCC N)=0    ⊃I 22 25 

27  ∀N.((N-N)=0⊃(SUCC N-SUCC N)=0)    ∀I 26 N ← N 

28  ∀N.(N-N)=0    TAUT